i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), snd:msg-spec(ds; da).
msg-spec-loc-decl(snd; i; da)  prop{i:l} 

latex

Definitions

void, Type, t  T, x:A. B(x), rcv(l,tg), Kind-deq, Knd, x.A(x), x. t(x), fpf-cap(f; eq; x; z), type List, ma-valtype(da; k), x:AB(x), decl-state(ds), , x:A  B(x), <a, b>, Id, t.1, msg-item(ds; da; k; l), fpf(A; a.B(a)), IdLnk, t.2, top, fpf-dom(eq; x; f), b, prop{i:l}, idlnk-deq, product-deq(A; B; a; b), P  Q, fpf-ap(f; eq; x), map(f; as), l_all(L; T; x.P(x)), source(l), s = t, P  Q, msg-spec-loc-decl(snd; i; da), msg-spec(ds; da)

Lemmas

lsrc wf, l all wf, map wf, fpf-ap wf, product-deq wf, idlnk-deq wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, msg-item wf, pi2 wf, IdLnk wf, fpf wf, pi1 wf, Id wf, nat wf, decl-state wf, ma-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf